structure REDUCE = struct
open GRAMMAR

(* =============================================================================================
 * Observation: if there are no primitive types in a rule's premise p, then the rule is guaranteed to succeed
 * if premise p and term t are type-unifiable and
 *   a. p has a type variable in it
 *   b. p has no type variables (is precise) and t is also precise
 * In such applications, there is no need to track failure term.
 *)
fun isPrim TyBool   = true
  | isPrim TyInt    = true
  | isPrim TyReal   = true
  | isPrim TyString = true
  | isPrim _        = false

fun isVar (TyVar _) = true
  | isVar  _        = false

fun hasPrimPremise (t as TyTerm _ ) = foldTy (fn (ty1,acc) => acc orelse isPrim ty1) (t,false)
  | hasPrimPremise (TyRule (lhs,_)) = foldTy (fn (ty1,acc) => acc orelse isPrim ty1) (lhs,false)
  | hasPrimPremise (TySum  (a,b)  ) = hasPrimPremise a orelse hasPrimPremise b
  | hasPrimPremise TyInf = false
  | hasPrimPremise arg = raise TypeError("Match failure in hasPrimPremise on arg: " ^ toString arg)

fun hasVarPremise  (t as TyTerm _ ) = foldTy (fn (ty1,acc) => acc orelse isVar ty1) (t,false)
  | hasVarPremise  (TyRule (lhs,_)) = foldTy (fn (ty1,acc) => acc orelse isVar ty1) (lhs,false)
  | hasVarPremise  (TySum  (a,b)  ) = hasVarPremise a orelse hasVarPremise b
  | hasVarPremise  TyInf = false
  | hasVarPremise  arg = raise TypeError("Match failure in hasVarPremise on arg: " ^ toString arg)

fun isPrecise ty1 = not (hasPrimPremise ty1) andalso not (hasVarPremise ty1)

(* =============================================================================================
 * Compare the order of two strategies and raise an error if the orders are not equal.
 * ============================================================================================= *)
fun getOrder (TyRule (_,TyVar _)) = 1
  | getOrder (TyRule (_,nonVar )) = 1 + getOrder nonVar
  | getOrder (TySum  (t1,t2)) = Int.min(getOrder t1, getOrder t2)
  | getOrder (TyList  ts)     = foldl (fn (a,acc) => if getOrder a < acc then getOrder a else acc ) (valOf(Int.maxInt)) ts
  | getOrder (TyMap  ty1    ) = getOrder ty1
  | getOrder (TyIter (_,ty1)) = getOrder ty1
  | getOrder (TyVar   _     ) = ~1
  | getOrder _                = 0

fun checkOrder (TyInf       , _          ) _ = () (* ignore unsupported constructs *)
  | checkOrder ( _          , TyInf      ) _ = ()
  | checkOrder (a as TyError, b          ) p = raiseCompositionError a b p "left operand contains a type error"
  | checkOrder (a           ,b as TyError) p = raiseCompositionError a b p "right operand contains a type error"
  | checkOrder (TyVar  _    , _          ) _ = ()
  | checkOrder ( _          , TyVar _    ) _ = ()
  | checkOrder (TyRule (_,b), TyRule(_,d)) expr = checkOrder(b,d) expr
  | checkOrder (a           , TySum (b,c)) expr = (checkOrder(a,b) expr; checkOrder(a,c) expr)
  | checkOrder (TySum  (a,b), c          ) expr = (checkOrder(a,c) expr; checkOrder(b,c) expr)
  | checkOrder (ty1,ty2) expr
      = let
            val ord1 = getOrder ty1
            val ord2 = getOrder ty2
        in
            if ord1 = ~1 orelse ord2 = ~1
            then ()
            else if ord1 = ord2
                 then ()
                 else raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: the order of operands must be the same; use foldS otherwise:" ^ crlf ^
                        "  left operand:  " ^ toString ty1 ^ crlf ^
                        "  right operand: " ^ toString ty2 ^ crlf ^
                        "  in expression: " ^ A.leavesToString expr false)
        end

fun stripFailTerm (      TySum (rhs, TyRule (TyVar _, TyVar _) )) = rhs (* omit SKIPs *)
  | stripFailTerm (p2 as TySum (_,   TyRule  _ )) = p2
  | stripFailTerm (p2 as TySum (_,   TySum   _ )) = p2
  | stripFailTerm (      TySum (rhs, failTerm  )) = rhs
  | stripFailTerm anyTy                           = anyTy

(* Checks if rule r is guaranteed to apply to term t *)
fun willApply r t = hasVarPremise r orelse hasVarPremise t orelse (isPrecise r andalso isPrecise t)

(* =============================================================================================
 * Computes the type of applying a strategy to a term.
 * reduce: (ty * ty * ctx) -> EXPR -> ty
 * ============================================================================================= *)
fun reduce(TyInf, _, e) _ = (TyInf, e)
  | reduce(r as TyRule (lhs,TyList _), t, env) p
    = raise TypeError(ninfoToString (A.getExprInfo p) ^
                            "Type error: applying higher-order rule without fold or foldS:" ^ crlf ^
                            "  rule:          " ^ toString r ^ crlf ^
                            "  argument term: " ^ toString t ^ crlf ^
                            "  in expression: " ^ A.leavesToString p false)

  | reduce(s as TyVar _, t, env) p (* applying a strategy of unknown type *)
    = let
          val _ = debug("reduce(tyvar): applying " ^ toString s ^ " to " ^ toString t) 1
          val rule1 = TyRule(nextVar(), nextVar())
          val (tyOut, env2) = reduce(rule1, t, env) p
          val envOut = if !precision = 0
                       then env2
                       else unify(s, [applySubst env2 rule1], env2, p)
          val _ = debug("reduce(tyvar): argument strategy after unification is " ^ toString (applySubst envOut s)) 0
          val _ = debug("reduce(tyvar): result is " ^ toString tyOut) ~1
      in
          (tyOut, envOut)
      end

  | reduce(r as TyRule (lhs as TyTerm (_,[TySome _]), rhs as TyTerm (_,[TySome _])), t as TyTerm(root,[TyVar z]), env) p
    = let
          val _ = debug("reduce: applying " ^ toString r ^ " to " ^ toString t) 1
          val envOut = unify (t, [lhs], env, p)
          val tyOut = applySubst envOut rhs
          val _ = debug("reduce: result is " ^ toString tyOut) ~1
      in
          (tyOut, envOut)
      end
  | reduce(r as TyRule (lhs as TyTerm (_,[TySome a]), rhs as TyTerm (_,[TySome b])), t as TyTerm(root,kids), env) p
    = let
          val _ = debug("reduce: applying " ^ toString r ^ " to " ^ toString t) 1
          val env2 = unify (t, [lhs], env, p)
          val rhs2 = applySubst env2 rhs
          val rhsF = applySubst env2 b
          val lhsF = applySubst env2 a
          val r2 = TyRule(lhsF,rhsF)
          fun mapReduce acc e (x::xs)
              = let
                    val (tyX,_) = reduce(r2, x, e) p handle TypeError _ => (x,e)
                in  
                    mapReduce (tyX::acc) e xs
                end
            | mapReduce acc e [] = (List.rev acc, e)
          val (newKids,envOut) = mapReduce [] env kids
          val newTerms = map (fn aList => TyTerm(root,aList)) (flattenSums [[]] newKids)
          val validTerms = List.filter isParseable newTerms
          val _ = if List.length validTerms = 0
                  then raiseAppError r2 t p "application cannot produce a term with valid structure"
                  else ()
          val tyOut = foldl (fn (term,acc) => TySum(acc,term)) (hd validTerms) (tl validTerms)
          val _ = debug("reduce: result is " ^ toString tyOut) ~1
      in
          (tyOut,env2)
      end
  | reduce(r as TyRule (lhs,rhs), t, env) p
    = let
          val _ = debug("reduce(rule): applying " ^ toString r ^ " to " ^ toString t) 1
          val env2 = unify (t, [lhs], env, p)
          val rhs2 = applySubst env2 rhs
          val (tyOut, envOut)
                = case getOrder rhs of
                    0 => if willApply r t
                         then (rhs2, env2)
                         else if rhs2 = t
                              then (rhs2, env2)
                              else (TySum (rhs2,t), env2)
                  | _ => (rhs2, env2)    (* for optimization, do not include SKIPs *)
          val _ = debug("reduce(rule): result is " ^ toString tyOut) ~1
      in
          (tyOut, envOut)
      end
  | reduce(s as TySum (a,b), t, env) p
    = let (* skip rules with incompatible types *)
          val (illTyped1, (rhs1, env1)) = (false, reduce (a,t,env) p) handle TypeError _ => (true, (t, env))
          val (illTyped2, (rhs2, env2)) = (false, reduce (b,t,env) p) handle TypeError _ => (true, (t, env))
          val sharedEnv = intersect (env1,env2)
          val isHetero = #1( (false, checkOrder (rhs1,rhs2) p) handle TypeError _ => (true, ()) )
      in
          if illTyped1 andalso illTyped2 then raiseAppError s t p "unexpected arguments in strategy application"
          else if illTyped1 then (rhs2, env2)
          else if illTyped2 then (rhs1, env1)
          else if isHetero then (TySum (rhs1, rhs2), sharedEnv)
          else if willApply a t orelse willApply b t (* 1 rule is guaranteed to succeed *)
               then (TySum (rhs1, rhs2), sharedEnv) (* leave results as they are *)
               else (TySum(TySum (stripFailTerm rhs1, stripFailTerm rhs2), t), sharedEnv) (* turn two fail-terms into 1 *)
      end

  (*** MAP ***)
  | reduce(TyMap _, t as TyTerm(_,[]), env) _ = (t,env) (* base case: no immediate subterms *)
  | reduce(TyMap(r as TyRule(_,TyRule _)), TyTerm(_,[one]), env) p = reduce(r, one, env) p
  | reduce(s as TyMap(TyRule(_,TyRule _)), t as TyTerm(_,xs), _) p  (* higher-order rule, multiple kids *)
      = raiseAppError s t p "generated strategies must be composed using fold/foldS"
  | reduce(s as TyMap(r as TyRule(a, b)), t as TyTerm(root,[TyVar z]), env) p
      = let
          val _ = debug("reduce.tymap-tyrule-tyvar. input: " ^ toString s ^ " | " ^ toString t) 1
          val _ = case root of
                    "'term" => () (* do not check generic nodes *)
                  | _ => let val regexOption = look(!tgtGrammar, root)
                         in  if not (isSome regexOption)
                             then raiseTypeError p ("Node " ^ root ^ " does not have rewritable children")
                             else case a of
                                    TyTerm(aRoot,_) =>
                                      if not (existsString aRoot (valOf regexOption))
		                                  then raiseAppError s t p "there are no suitable subterms for mapX to apply to"
		                                  else (case b of 
		                                         TyTerm(bRoot,_) =>
		                                           if not (existsString bRoot (valOf regexOption))
				                                       then raiseAppError s t p "application cannot produce a term with valid structure"
				                                       else ()
				                                   | _ => ())
				                          | _ => ()
                         end
          val tyIn   = TyTerm(root,[TySome a])
          val tyOut  = if hasPrimPremise a
                       then TySum(TyTerm(root,[TySome b]), tyIn)
                       else TyTerm(root,[TySome b])
          val envOut = unify(TyVar z, [tyIn], env, p)
          val _ = debug("reduce.tymap-tyrule-tyvar.output: " ^ toString tyOut) ~1
        in
          (tyOut, envOut)
        end
  | reduce(s as TyMap(r as TyRule _), t as TyTerm(root,kids), env) p
    = let
          val _ = debug("reduce.tymap-tyrule-kids. input: " ^ toString s ^ " | " ^ toString t) 1
          val mapApplied = ref 0
          fun inc() = mapApplied := !mapApplied + 1
          fun mapReduce acc e (x::xs)
              = let
                  val (applied,(tyX,envX)) = (true, reduce(r,x,e) p) handle
                                               TypeError _ => (false, (x,e))
                in  if applied
                    then (inc(); mapReduce (tyX::acc) envX xs)
                    else mapReduce (x::acc) e xs
                end
            | mapReduce acc e [] = (List.rev acc, e)
          val (newKids, envF) = mapReduce [] env kids
          val _ = if (!mapApplied = 0)
                  then raiseAppError s t p "there are no suitable subterms to apply to"
                  else ()
          val newTerms = map (fn aList => TyTerm(root,aList)) (flattenSums [[]] newKids)
          val validTerms = List.filter isParseable newTerms
          val _ = if List.length validTerms = 0
                  then raiseAppError s t p "application cannot produce a term with valid structure"
                  else ()
          val tyF = foldl (fn (term,acc) => TySum(acc,term)) (hd validTerms) (tl validTerms)
          val _ = debug("reduce.tymap-tyrule-kids.output: " ^ toString tyF) ~1
      in
          (tyF, envF)
      end
  | reduce(s as TyMap(TySum(a,b)), t, e) p
    = let
          val _ = debug("reduce.tymap-tysum. input: " ^ toString s ^ " | " ^ toString t) 1
          val (illTyped1, (t1, e1)) = (false, reduce(TyMap a, t, e) p) handle TypeError _ => (true, (t, e))
          val (illTyped2, (t2, e2)) = (false, reduce(TyMap b, t, e) p) handle TypeError _ => (true, (t, e))
		      val (tyF, eF) = if illTyped1 andalso illTyped2 then raiseAppError s t p "unexpected arguments in strategy application"
								          else if illTyped1 then (t2, e2)
								          else if illTyped2 then (t1, e1)
								          else (TySum (t1, t2), intersect (e1, e2))
          val _ = debug("reduce.tymap-tysum.output: " ^ toString tyF) ~1
      in
          (tyF, eF)
      end

  (*** ITERATOR ***)
  | reduce(s as TyIter ("FIX", r as TyRule(TyTerm(lhs,_),TyTerm(rhs,_))), t, env) p
    = let
          val (ty2, e2) = reduce(r, t, env) p
      in
          if lhs = rhs
          then (ty2, e2)
          else raise TypeError(ninfoToString (A.getExprInfo p) ^
                 "Type error: the type of FIX must be (T->T)->T (e.g. (expr->expr)->expr)" ^ crlf ^
                 "  iterator expression: " ^ toString s ^ crlf ^
                 "  argument term:       " ^ toString t ^ crlf ^
                 "  in expression:       " ^ A.leavesToString p false)
      end
  | reduce(TyIter (_, TyRule(TyVar _, TyVar _)), t as TyTerm _, env) _ = (t,env) (* ID/SKIP *)
  | reduce(TyIter (F, TyIter("FIX", s2)), t, env) p = reduce(TyIter(F,s2), t, env) p (* e.g. TDL (FIX r) t *)
  | reduce(s as TyIter (_, r as TyRule(lhs as TyTerm(x,_),rhs as TyTerm(y,_))), t, env) p
    = let
        val appCounter = ref 1
        fun trav (term as TyTerm(root,[TyVar _])) ctx (* argument term (tyT) structure is unknown *)
            = let
                (*val (unified, ctx2) = (true, unify(term,[lhs],ctx,p)) handle TypeError _ => (false,ctx)
                val (term1, ctx3) = if unified
                                    then (appCounter := !appCounter + 1; (applySubst ctx2 rhs, ctx2))
                                    else (term, ctx2)*)
              in
                (*if unified orelse (isDerivable x root [] andalso isDerivable y root [])
                then (appCounter := !appCounter + 1; (term1,ctx3))
                else raise TypeError(ninfoToString (A.getExprInfo p) ^
                        "Type error: lhs or rhs of the rule don't exist in argument term's structure" ^ crlf ^
                        "  iterator:      " ^ toString s ^ crlf ^
                        "  rewrite rule:  " ^ toString r    ^ crlf ^
                        "  local term:    " ^ toString term ^ crlf ^
                        "  argument term: " ^ toString t    ^ crlf ^
                        "  in expression: " ^ A.leavesToString p false)*)
                (TyTerm(root,[nextVar()]), ctx)
              end
          | trav (term as TyTerm(root,kids)) ctx
            = let
                fun aux e acc (k::ks)
                    = let
                        val (k2,e1) = trav k e (* bottom-up *)
                        (*val _ = if isParseable (TyTerm (root,List.rev(k2::acc)@ks))
                                then ()
                                else appCounter := !appCounter - 1*)
                      in
                        aux e1 (k2::acc) ks
                      end
                  | aux e acc [] = (List.rev acc, e)
                val (kids2, ctx2) = aux ctx [] kids
                (*val (unified, ctx3) = (true, unify(term,[lhs],ctx2,p)) handle TypeError _ => (false,ctx2)*)
              in
                (*if unified
                then (appCounter := !appCounter + 1; (applySubst ctx3 rhs, ctx3))
                else*) (TyTerm(root,kids2), ctx2)
              end
          | trav term ctx = (term,ctx)
        val (newTerm, env2) = trav t env
      in
        if (!appCounter > 0)
        then (newTerm, env2)
        else raise TypeError(ninfoToString (A.getExprInfo p) ^
               "Type error: iterator cannot successfully modify any subterm of the argument term " ^ crlf ^
               "  iterator:      " ^ toString s ^ crlf ^
               "  argument term: " ^ toString t ^ crlf ^
               "  in expression: " ^ A.leavesToString p false)
      end

  | reduce(TyIter(F,TySum(a,b)), t, env) p
    = let
          val (ty1,_) = reduce(TyIter(F,a), t, env) p
          val (ty2,_) = reduce(TyIter(F,b), t, env) p
      in
          (TySum(ty1,ty2),env)
      end

  | reduce(s as TyIter (F, r as TyRule(lhs as TyTerm(x,_),rhs)), t, env) p
    = let
        val appCounter = ref 1
        fun trav (term as TyTerm(root,[TyVar _])) ctx (* argument term's structure is unknown *)
            = let
                val (unified, ctx2) = (true, unify(term,[lhs],ctx,p)) handle TypeError _ => (false,ctx)
                val (rules, ctx3) = if unified
                                    then ([applySubst ctx2 rhs], ctx2)
                                    else ([TyRule(nextVar(), nextVar())], ctx2)
              in
                (*if unified orelse isDerivable x root []
                then (appCounter := !appCounter + 1; (rules,ctx3))
                else raise TypeError(ninfoToString (A.getExprInfo p) ^
                        "Type error: lhs of the higher-order rule does not exist in the argument term's "^
                        "structure" ^ crlf ^
                        "  iterator:      " ^ toString s ^ crlf ^
                        "  rewrite rule:  " ^ toString r ^ crlf ^
                        "  argument term: " ^ toString t ^ crlf ^
                        "  in expression: " ^ A.leavesToString p false)*)
                (rules, ctx3)
              end
          | trav (term as TyTerm(_,kids)) ctx
            = let
                fun aux e acc (k::ks)
                    = let
                        val (s1,e1) = trav k e
                      in
                        aux e1 (s1@acc) ks
                      end
                  | aux e acc [] = (List.rev acc, e)
                val (rules, ctx2) = aux ctx [] kids
                val (unified, ctx3) = (true, unify(term,[lhs],ctx2,p)) handle TypeError _ => (false,ctx2)
                val rules2 = if unified
                             then (appCounter := !appCounter + 1; ((applySubst ctx3 rhs)::rules))
                             else rules
              in
                (rules2,ctx3)
              end
          | trav _ ctx = ([],ctx)
        val (strats,env2) = trav t env
        (*val _ = print1(foldr (op ^) "" (map toString strats))*)
        (*fun comp(x,y) = #1(case F of
                         "lcond_tdl"    => createComp "<+" x y env2 p
                       | "lcond_tdr"    => createComp "<+" x y env2 p
                       | "lcond_bul"    => createComp "<+" x y env2 p
                       | "lcond_bur"    => createComp "<+" x y env2 p
                       | "rcond_tdl"    => createComp "+>" x y env2 p
                       | "rcond_tdr"    => createComp "+>" x y env2 p
                       | "rcond_bul"    => createComp "+>" x y env2 p
                       | "rcond_bur"    => createComp "+>" x y env2 p
                       |  "lseq_tdl"    => createComp "<;" x y env2 p
                       |  "lseq_tdr"    => createComp "<;" x y env2 p
                       |  "lseq_bul"    => createComp "<;" x y env2 p
                       |  "lseq_bur"    => createComp "<;" x y env2 p
                       |  "rseq_tdl"    => createComp ";>" x y env2 p
                       |  "rseq_tdr"    => createComp ";>" x y env2 p
                       |  "rseq_bul"    => createComp ";>" x y env2 p
                       |  "rseq_bur"    => createComp ";>" x y env2 p
                       | "lconjunct_tdl"=> createComp "<*" x y env2 p
                       | "lstar_tdr"    => createComp "<*" x y env2 p
                       | "lstar_bul"    => createComp "<*" x y env2 p
                       | "lstar_bur"    => createComp "<*" x y env2 p
                       | "rconjunct_tdl"=> createComp "*>" x y env2 p
                       | "rstar_tdr"    => createComp "*>" x y env2 p
                       | "rstar_bul"    => createComp "*>" x y env2 p
                       | _              => createComp "*>" x y env2 p)
                       *)
      in
        if (!appCounter > 0)
        then (*(foldl comp (hd strats) (tl strats),env2)*)
             (TyRule(nextVar(), nextVar()),env2)
        else raise TypeError(ninfoToString (A.getExprInfo p) ^
               "Type error: iterator cannot successfully generate any new dynamic rules" ^ crlf ^
               "  iterator:      " ^ toString s ^ crlf ^
               "  argument term: " ^ toString t ^ crlf ^
               "  in expression: " ^ A.leavesToString p false)
      end

  (*** Custom traversals ***)
  | reduce(TyRec (_, [], body), t, env) p (* custom traversal: 1 arg *)
    = reduce(body,t,env) p
  | reduce(TyRec (F, x::xs, body), t, env) p
    = let
        val (unified, env2) = (true, unify(t,[x],env,p)) handle TypeError _ => (false,env)
      in
        if unified then (TyRec (F, xs, applySubst env2 body),env2)
        else raise TypeError(ninfoToString (A.getExprInfo p) ^
                            "Type error: unexpected argument in recursive iterator application:" ^ crlf ^
                            "  expected: " ^ toString x ^ crlf ^
                            "  received: " ^ toString t ^ crlf ^
                            "  in expression: " ^ A.leavesToString p false)
      end

  | reduce(s, t, _) p = raiseAppError s t p "unexpected arguments in strategy application"

end